#include "../FileManager/Lex_byacc/cnf_reader.cuh"
#include "../FileManager/ParametersManager.cuh"
#include "Parallelizer.cuh"
#include "../JobsManager/JobChooser.cuh"
#include "../FileManager/FileUtils.cuh"
#include "Results.cuh"
#include <stdio.h>
#include <assert.h>
#include <vector>
#include <string.h>
#include "Configs.cuh"
#include "../Statistics/RuntimeStatistics.cuh"
#include "../ErrorHandler/CudaMemoryErrorHandler.cuh"
#include "../JobsManager/SimpleJobChooser.cuh"

using namespace std;



void print_info(int& number_of_blocks, int& number_of_threads,
		ParametersManager& pm, int& number_of_variables, int& number_of_clauses,
		FormulaData& for_data, int& max_implication_per_var) {
	if (number_of_blocks < 1) {
		printf("Invalid number of blocks: %d\n", number_of_blocks);
	}
	if (number_of_threads < 1) {
		printf("Invalid number of threads: %d\n", number_of_threads);
		exit(1);
	}
	if (pm.get_verbosity_level() >= 1) {
		printf("Solver configuration:\n");
		printf("Input file: %s\n", pm.get_input_file());
		printf("Formula has %d variables and %d clauses\n", number_of_variables,
				number_of_clauses);
		printf("Variable '%d', the most frequent, has been found %d times.\n",
				for_data.get_most_common_variable() + 1,
				for_data.get_frequency_of_most_common_variable());
		if (pm.get_number_of_threads() == 1
				&& !pm.get_sequential_as_parallel()) {
			printf("Parallelization strategy: SEQUENTIAL RUN\n");
		} else {
			printf("Parallelization strategy: Divide and Conquer\n");
			printf("Number of blocks: %d\n", pm.get_number_of_blocks());
			printf("Number of threads: %d\n", pm.get_number_of_threads());
			switch (pm.get_choosing_strategy()) {
			case DISTRIBUTE_JOBS_PER_THREAD:
				printf("Job creation strategy: distribution per thread\n");
				break;
			case UNIFORM:
				printf("Job creation strategy: uniform\n");
				break;
			default:
				printf("Unknown job creation strategy!\n");
				break;
			}
		}

		printf("Conflict analysis: ON with");
		printf("out");
		printf(" forward edges\n");
		printf("Capacity of edges = %d\n", max_implication_per_var);
		printf("Assumptions are stored in a ");
		printf("statically");
		printf(" allocated vector.\n");
		printf("Formula clauses are stored in ");
		printf("several allocations.\n");
		printf("Unary clauses pre-processing is %s\n", pm.get_preprocess_unary_clauses()
				? "ON" : "OFF");
		printf("Conflict analysis is ");
		switch (CONFLICT_ANALYSIS_STRATEGY) {
			case BASIC_SEARCH:
				printf("basic search\n");
				break;
			case FULL_SPACE_SEARCH:
				printf("full space search\n");
				break;
			case TWO_WATCHED_LITERALS:
				printf("two wached literals\n");
				break;
			default:
				printf("unknown!\n");
				break;
		}
	}
	printf("VSIDS is ");
#ifdef USE_VSIDS
	printf("ON\n");
#else
	printf("OFF\n");
#endif
	printf("Restart is ");
#ifdef USE_RESTART
	printf("ON\n");
#else
	printf("OFF\n");
#endif
	printf("Clause learning is ");
#ifdef USE_CLAUSE_LEARNING
	printf("ON with learnt clause capacity of %d\n", MAX_LEARNT_CLAUSES_PER_THREAD);
#else
	printf("OFF\n");
#endif
	printf("Simple jobs generation is ");
#ifdef USE_SIMPLE_JOBS_GENERATION
	printf("ON\n");
#else
	printf("OFF\n");
#endif
}

int main(int argc, char** argv)
{

	ParametersManager pm(argc, argv);

	if(!pm.valid_parameters() || pm.has_help_parameter())
	{
		if(pm.get_input_file() == NULL && !pm.has_help_parameter())
		{
			printf("Missing input file or '-h' parameter!\n");
		}

		if(pm.get_unknown_parameter() != '\0')
		{
			printf("Parameter -%c is unknown!\n", pm.get_unknown_parameter());
		}

		pm.print_help(argv);
		exit(pm.valid_parameters() ? 0 : 1);
	}

	if(!file_exists(pm.get_input_file()))
	{
		printf("The specified CNF file (%s) was not found!\n", pm.get_input_file());
		exit(1);
	}

	if(pm.get_output_file() != NULL && !file_exists(pm.get_output_file()))
	{
		printf("The specified output file (%s) was not found!\n", pm.get_output_file());
		exit(1);
	}

	int lines = number_of_lines(pm.get_input_file());

	CUDAClauseVec formula(lines);
	vector < Clause > formula_host;

	int number_of_variables;
	int number_of_clauses;

	FormulaData for_data(lines, pm.get_preprocess_unary_clauses());

	bool success = read_cnf(pm.get_input_file(), for_data);

	if(for_data.get_number_of_variables() < MIN_VARIABLES_TO_PARALLELIZE &&
			(pm.get_number_of_blocks() > 1 || pm.get_number_of_threads() > 1 ||
					pm.get_sequential_as_parallel()))
	{
		printf("Warning: There are %d variables in the formula and at least %d "
				"are necessary to parallelize. Forcing sequential execution!\n",
				for_data.get_number_of_variables(), MIN_VARIABLES_TO_PARALLELIZE);
		pm.force_sequential_configuration();
	}

	formula = for_data.get_formula_dev();
	formula_host = *(for_data.get_formula_host());
	number_of_variables = for_data.get_number_of_variables();
	number_of_clauses = for_data.get_number_of_clauses();

	int number_of_threads = pm.get_number_of_threads();
	int number_of_blocks = pm.get_number_of_blocks();

	// This holds the max implication a variable may have, to set the capacity of edges.
	int max_implication_per_var;

	max_implication_per_var = for_data.get_largest_clause_size();

	if(max_implication_per_var < MIN_IMPLICATION_PER_VAR)
		max_implication_per_var = MIN_IMPLICATION_PER_VAR;

	print_info(number_of_blocks, number_of_threads, pm, number_of_variables,
			number_of_clauses, for_data, max_implication_per_var);

	if(for_data.get_status_after_preprocessing() != UNDEF)
	{
		if(pm.get_verbosity_level() >= 1)
		{
			printf("Solved in pre-processing.\n");
		}
		Results res(number_of_variables, false);
		res.set_host_status(for_data.get_status_after_preprocessing());
		res.print_results((*for_data.get_set_literals()));
		return 0;
	}


	vector <Lit> * set_lits = for_data.get_set_literals();
	GPUVec<Var> dv(set_lits->size());
	vector<Var> dead_vars_host;

	for(std::vector<Lit>::iterator it = set_lits->begin(); it != set_lits->end(); ++it)
	{
		dv.add(var(*it));
		dead_vars_host.push_back(var(*it));
	}
	GPUVec<Var> * dead_vars = &dv;

	// Original assumptions!
	GPUVec<Lit> assumptions(0);

	float   elapsedTime;

	if(success)
	{
		Results * results_dev;
		DataToDevice * data_ptr;

		if(number_of_threads == 1 && number_of_blocks == 1 && !pm.get_sequential_as_parallel())
		{
			if(pm.get_verbosity_level() >= 1)
			{
				printf("Number of jobs = 1\n");
			}
#ifdef DEBUG
			printf("About to call sequential kernel!\n");
#endif

			DataToDevice data(formula, number_of_variables, number_of_clauses,
					1, 1, 1, max_implication_per_var, *dead_vars);
			data_ptr = &data;

			data.prepare_sequencial();

			cudaEvent_t     start, stop;
			cudaEventCreate( &start );
			cudaEventCreate( &stop );
			cudaEventRecord( start, 0 );
			run_sequential<<<1,1>>>(data);

			cudaEventRecord( stop, 0 );
			cudaEventSynchronize( stop );
			cudaEventElapsedTime( &elapsedTime,
			                       start, stop );
			cudaEventDestroy( start );
			cudaEventDestroy( stop );

			results_dev = data.get_results_ptr();

		}
		else
		{
#ifdef USE_SIMPLE_JOBS_GENERATION
			SimpleJobChooser jc(&formula_host, number_of_variables, &dead_vars_host);
#else
			MaxClauseJobChooser
			jc(&formula_host, number_of_variables,
					dead_vars->size_of(), number_of_threads,
					number_of_blocks, pm.get_choosing_strategy());
#endif
			JobChooser * chooser = &jc;

			chooser->evaluate();

			int number_of_jobs = chooser->get_number_of_jobs();


			if(pm.get_verbosity_level() >= 1)
			{
				printf("Number of jobs = %d\n", number_of_jobs);
			}

#ifdef DEBUG

			printf("About to call parallel kernel!\n");
#endif

			DataToDevice data(formula, number_of_variables, number_of_clauses,
					number_of_jobs,
					number_of_blocks, number_of_threads,
					//32, 1,
					max_implication_per_var, *dead_vars);
			data_ptr = &data;

			data.prepare_parallel(*chooser
#ifdef ASSUMPTIONS_USE_DYNAMICALLY_ALLOCATED_VECTOR
					, assumptions
#endif
					);

			check(cudaThreadSetLimit(cudaLimitMallocHeapSize, 1*1024*1024*1024),"Setting malloc heap size");
			cudaEvent_t     start, stop;
			cudaEventCreate( &start );
			cudaEventCreate( &stop );
			cudaEventRecord( start, 0 );

			run_parallel<<<number_of_blocks, number_of_threads>>>(data);
			//run_parallel<<<blocks, 1>>>(data);

			cudaEventRecord( stop, 0 );
			cudaEventSynchronize( stop );
			cudaEventElapsedTime( &elapsedTime,
			                         start, stop );
			cudaEventDestroy( start );
			cudaEventDestroy( stop );


			results_dev = data.get_results_ptr();

#ifdef ENABLE_STATISTICS
			int solved_jobs = data.get_statistics().get_all_threads_total_completed_jobs();

			if(results_dev->get_status() == UNSAT)
			{
				assert(solved_jobs == number_of_jobs);
			}

#ifdef DEBUG
			printf("Jobs size = %d\n", number_of_jobs);
			printf("There were %d jobs created.\nThere were %d solved jobs\n", number_of_jobs,solved_jobs);
#endif
#endif
		}

		cudaDeviceSynchronize();
#ifdef ENABLE_STATISTICS
		if(pm.get_verbosity_level() >= 2)
		{
			data_ptr->get_statistics().print_function_time_statistics();
			printf("Total time in GPU: %f\n", elapsedTime);
		}
#endif

		results_dev->print_results(*(for_data.get_set_literals()));

		cudaDeviceReset();


	}
	else
	{
		printf("The provided CNF formula is not valid!\n");
		exit(2);
	}


	return 0;

}
